/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#3=SUB/FONT#4=SUP/FONT#5=GACS25/FONT#6=FIX20/FONT#7=SYMB30[FNT,CLT]/FONT#8=FIX25/FONT#11=GRFX25/FONT#12=GRFX35



␈↓ ↓H␈↓αInformal description of a possible solution to the "component of a graph" problem.

␈↓ ↓H␈↓        Assume␈α∞the␈α∞function␈α∞␈↓↓successors␈↓␈α
represents␈α∞a␈α∞finite␈α∞graph␈α
G.␈α∞ We␈α∞introduce␈α∞a␈α∞sort␈α
␈↓↓isvertex␈↓
␈↓ ↓H␈↓intended␈α∞to␈α∂test␈α∞if␈α∂an␈α∞individual␈α∞is␈α∂a␈α∞vertex␈α∂in␈α∞G,␈α∞and␈α∂let␈α∞the␈α∂variables␈α∞␈↓↓a,␈↓␈α∞␈↓↓b,␈↓␈α∂␈↓↓c␈↓␈α∞...␈α∂range␈α∞over
␈↓ ↓H␈↓vertices of G.  We define some predicates useful in discussing graphs.

␈↓ ↓H␈↓␈↓↓∀a b u: [path[a, b, u] ≡ ¬␈↓αn|␈↓↓u ∧ ␈↓αa|␈↓↓u = b ∧ [[␈↓αn|␈↓↓␈↓αd|␈↓↓u ∧ a = b]  ∨ isvertex ␈↓αad|␈↓↓u ∧ path[a, ␈↓αad|␈↓↓u, ␈↓αd|␈↓↓u]]]␈↓

␈↓ ↓H␈↓␈↓↓path␈↓ gives the criterion for a list ␈↓↓u␈↓ to represent a path from ␈↓↓a␈↓ to ␈↓↓b␈↓ in G.

␈↓ ↓H␈↓        ␈↓↓∀a b n: [gamma [a, b, n] ≡ [n=0 ∧ a=b] ␈↓
␈↓ ↓H␈↓                        ␈↓↓∨ [∃c: [gamma[a, c, n-1] ∧ a ε successors c] ␈↓
␈↓ ↓H␈↓                        ␈↓↓∧ ∀m: [m < n ⊃ ¬gamma[a, b, m]]]]␈↓

␈↓ ↓H␈↓        ␈↓↓∀a b: [incomponent[a, b] ≡ ∃u: path[a, b, u]]␈↓


␈↓ ↓H␈↓By induction on ␈↓↓n␈↓ one can prove

␈↓ ↓H␈↓        (i) ␈↓↓∀a b n: [gamma[a, b, n] ⊃ ∃u: [path[a, b, u] ∧ length u = n+1]]␈↓

␈↓ ↓H␈↓By induction on ␈↓↓length u␈↓ one can prove

␈↓ ↓H␈↓        (ii) ␈↓↓∀a b u: [path[a, b, u] ⊃ ∃n: [n<length u ∧ gamma[a, b, n]]]␈↓

␈↓ ↓H␈↓From (i) and (ii) we conclude that

␈↓ ↓H␈↓        (iii) ␈↓↓∀a b: [∃u: path[a, b, u] ≡ ∃n: gamma[a, b, n]]␈↓

␈↓ ↓H␈↓and hence

␈↓ ↓H␈↓        (iv) ␈↓↓∀a b: [incomponent[a, b] ≡ ∃n: gamma[a, b, n]]␈↓

␈↓ ↓H␈↓Now we wish to define a function ␈↓↓component␈↓ on vertices such that

␈↓ ↓H␈↓        (v) ␈↓↓∀a b: [b ε component[a] ≡ ∃n: gamma [a, b, n]]␈↓

␈↓ ↓H␈↓For the present we assume that finiteness of the graph G means

␈↓ ↓H␈↓FIN     ␈↓↓∀a: ∃l: ∀m: [[m≥l ⊃ ∀b: ¬gamma[a, b, l]] ∧ [m<l ⊃ ∃b: gamma[a, b, m]]]␈↓

␈↓ ↓H␈↓Define the function computing the component of a vertex as follows (assume ␈↓↓seen␈↓ is of sort list)

␈↓ ↓H␈↓        ␈↓↓∀a: [component a = comp[<a>, ␈↓¬NIL␈↓↓]]␈↓

␈↓ ↓H␈↓        ␈↓↓∀u seen: [comp[u,seen] = ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ seen ␈↓αelse␈↓↓ comp[gam[u]~seen, u*seen]]␈↓

␈↓ ↓H␈↓        ␈↓↓∀u: [gam[u] = ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ successors ␈↓αa|␈↓↓u * gam[␈↓αd|␈↓↓u]]␈↓

␈↓ ↓H␈↓We␈α∞now␈α
show␈α∞␈↓↓∀a:␈α∞islist␈α
component␈α∞a␈↓␈α
 and␈α∞␈↓↓∀a␈α∞b:␈α
[b␈α∞ε␈α
component␈α∞a␈α∞≡␈α
incomponent[a,␈α∞b]]␈↓.␈α∞ This␈α
is
␈↓ ↓H␈↓done by using CVI induction with
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓        ␈↓↓␈↓πF␈↓↓(n) ≡ ∀u seen: [[∀b: [b ε u ≡ gamma[a, b, N-n]] ␈↓
␈↓ ↓H␈↓                    ␈↓↓∧ ∀b: [b ε seen ≡ ∃m: m<N-n ∧ gamma[a, b, m]]]␈↓
␈↓ ↓H␈↓                        ␈↓↓⊃ islist comp[u, seen] ∧ ∀b: [b ε comp[u, seen] ≡ ∃n: gamma[a, b, n]]]␈↓

␈↓ ↓H␈↓where␈α
␈↓↓N␈↓␈α∞is␈α
the␈α
bound␈α∞guaranteed␈α
by␈α
FIN.␈α∞ Briefly␈α
this␈α
goes␈α∞as␈α
follows.␈α
 In␈α∞the␈α
case␈α∞n=0,␈α
using
␈↓ ↓H␈↓FIN␈αwe␈αhave␈α␈↓↓u␈↓␈α=␈α␈↓¬NIL␈↓␈αand␈αby␈αthe␈αhypothesis␈αon␈α␈↓↓seen␈↓␈αthe␈αresult␈αfollows.␈α If␈α␈↓↓n>0␈↓␈α then␈αby␈αFIN␈α␈↓↓u␈↓␈α≠
␈↓ ↓H␈↓␈↓¬NIL␈↓ so ␈↓↓comp[u,seen]␈↓ reduces to ␈↓↓comp[gam[u]~seen, u*seen]␈↓.  With n1=n-1 we have

␈↓ ↓H␈↓        ␈↓↓∀b: [b ε gam[u]~seen ≡ gamma[a, b, N-n1]]␈↓

␈↓ ↓H␈↓        ␈↓↓∀b: [b ε u*seen ≡ ∃m: m<N-n1 ∧ gamma[a, b, m]]␈↓

␈↓ ↓H␈↓using␈α
properties␈αof␈α
␈↓↓u,␈↓␈α␈↓↓seen,␈↓␈α
and␈αthe␈α
definitions␈αof␈α
␈↓↓gam␈↓␈αand␈α
␈↓↓gamma␈↓␈αand␈α
so␈αthe␈α
conclusion␈α
of␈α␈↓πF␈↓
␈↓ ↓H␈↓holds.

␈↓ ↓H␈↓        Finally␈αwith␈α
␈↓↓n=N␈↓␈αand␈α
␈↓↓u=<a>␈↓␈αand␈α
␈↓↓seen=␈↓¬NIL␈↓↓␈↓␈αthe␈αhypothesis␈α
of␈α␈↓πF␈↓␈α
is␈αsatisfied␈α
so␈αwe␈αobtain␈α
the
␈↓ ↓H␈↓desired result using the definition of ␈↓↓component.␈↓


␈↓ ↓H␈↓αComments.

␈↓ ↓H␈↓        Some␈α
fixing␈α
has␈α
to␈α
be␈αdone␈α
to␈α
deal␈α
with␈α
the␈αpredicate␈α
definitions.␈α
 In␈α
fact␈α
it␈αwould␈α
probably
␈↓ ↓H␈↓be␈αeasier␈αto␈αreplace␈α␈↓↓gamma␈↓␈αby␈αa␈αfunction␈αthat␈αcomputes␈αthe␈αcorresponding␈αset.␈α  One␈αis␈αalso␈αlikely
␈↓ ↓H␈↓to have to fuss with the free variable ␈↓↓a␈↓ in the induction predicate to make FOL happy.


␈↓ ↓H␈↓αRevised description of a possible solution to the "component of a graph" problem.

␈↓ ↓H␈↓        Assume␈α∞the␈α∞function␈α∞␈↓↓successors␈↓␈α
represents␈α∞a␈α∞finite␈α∞graph␈α
G.␈α∞ We␈α∞introduce␈α∞a␈α∞sort␈α
␈↓↓isvertex␈↓
␈↓ ↓H␈↓intended␈α∞to␈α∂test␈α∞if␈α∂an␈α∞individual␈α∞is␈α∂a␈α∞vertex␈α∂in␈α∞G,␈α∞and␈α∂let␈α∞the␈α∂variables␈α∞␈↓↓a,␈↓␈α∞␈↓↓b,␈↓␈α∂␈↓↓c␈↓␈α∞...␈α∂range␈α∞over
␈↓ ↓H␈↓vertices of G.  We define some properties useful in discussing graphs.

␈↓ ↓H␈↓␈↓↓∀a b u: [path[a, b, u] ≡ ¬␈↓αn|␈↓↓u ∧ ␈↓αa|␈↓↓u = b ∧ [[␈↓αn|␈↓↓␈↓αd|␈↓↓u ∧ a = b]  ∨ isvertex ␈↓αad|␈↓↓u ∧ path[a, ␈↓αad|␈↓↓u, ␈↓αd|␈↓↓u]]]␈↓

␈↓ ↓H␈↓␈↓↓path␈↓ gives the criterion for a list ␈↓↓u␈↓ to represent a path from ␈↓↓a␈↓ to ␈↓↓b␈↓ in G.

␈↓ ↓H␈↓␈↓ ∧l␈↓↓∀w: [pathlength w = length w - 1]␈↓ 

␈↓ ↓H␈↓␈↓↓pathlength␈↓ is the length of the path represented by ␈↓↓w.␈↓

␈↓ ↓H␈↓␈↓ α{␈↓↓∀a l: [depth a = l ≡ [∃b w: [pathlength w = m ∧ path[a, b, w]] ≡ m < l]]␈↓ 

␈↓ ↓H␈↓␈↓↓depth␈↓␈α
gives␈α
the␈α
maximum␈α
distance␈αfrom␈α
a␈α
given␈α
vertex␈α
to␈αany␈α
connected␈α
vertex.␈α
  The␈α
fact␈αthat␈α
G
␈↓ ↓H␈↓is finite tells us that ␈↓↓depth␈↓ is defined for any vertex of G.  Thus we have

␈↓ ↓H␈↓␈↓¬FIN ␈↓   ␈↓ ¬Z␈↓↓∀a: ∃l: depth a =l␈↓ 

␈↓ ↓H␈↓The␈α∂condition␈α∂that␈α⊂a␈α∂vertex␈α∂␈↓↓b␈↓␈α⊂is␈α∂the␈α∂component␈α⊂of␈α∂␈↓↓a␈↓␈α∂(eg.␈α∂␈↓↓b␈↓␈α⊂is␈α∂connected␈α∂to␈α⊂␈↓↓a␈↓␈α∂is␈α∂given␈α⊂by␈α∂the
␈↓ ↓H␈↓predicate ␈↓↓incomponent␈↓ which is defined by

␈↓ ↓H␈↓␈↓ ∧≡␈↓↓∀a b:  [incomponent[a, b] ≡ ∃w: path[a, b, w]]␈↓ 
␈↓ ↓H␈↓␈↓ εH␈↓ 93


␈↓ ↓H␈↓We define a function to compute the set of vertices in the component of a given vertex by

␈↓ ↓H␈↓␈↓ ∧h␈↓↓∀a: [component a = comp[<a> ␈↓¬NIL␈↓↓]]␈↓ 

␈↓ ↓H␈↓␈↓ αI␈↓↓∀u seen: [comp[u,seen] = ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ seen ␈↓αelse␈↓↓ comp[slist u - u*seen , u*seen]]␈↓ 

␈↓ ↓H␈↓␈↓ β;␈↓↓∀u: [slist u = ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ [successors ␈↓αa|␈↓↓u] ∪ [slist ␈↓αd|␈↓↓u]]␈↓ 

␈↓ ↓H␈↓We would like to show that ␈↓↓component␈↓ is correct, namely that

␈↓ ↓H␈↓␈↓ ∧3␈↓↓∀a b: [b ε component a ≡ incomponent[a, b]]␈↓ 

␈↓ ↓H␈↓to do this we prove something about ␈↓↓comp␈↓ namely ␈↓↓∀n: ␈↓πF␈↓↓[n]␈↓

␈↓ ↓H␈↓␈↓↓∀a u seen:[[ n≤depth a ∧ ␈↓πF␈↓↓1[a, u, seen] ∧ ␈↓πF␈↓↓2[a, u, seen]]␈↓
␈↓ ↓H␈↓                ␈↓↓ ⊃ [islist comp[u, seen] ∧ ∀b: [bεcomp[u,seen] ≡ incomponent[a,b]]]]␈↓

␈↓ ↓H␈↓where

␈↓ ↓H␈↓␈↓ α+␈↓↓␈↓πF␈↓↓1[n, a, u, seen] ≡ ∀b: [b ε seen ≡ ∃w: [plength w + n < depth a ∧ path[a, b, w]]]]␈↓ 

␈↓ ↓H␈↓␈↓ ↓f␈↓↓␈↓πF␈↓↓2[n, a, u, seen] ≡ ∀b: [b ε u ≡ ¬[b ε seen] ∧ ∃w: [plength w + n = depth a  ∧ path[a, b, w]]]␈↓ 

␈↓ ↓H␈↓Clearly␈αif␈αwe␈αtake␈α␈↓↓n = depth a␈↓,␈α␈↓↓u = <a>␈αand␈αseen = ␈↓¬NIL␈↓↓␈αthen␈αthe␈αhypotheses␈αof␈α␈↓πF␈↓↓␈αare␈αsatisified␈αand
␈↓ ↓H␈↓↓this proves what we wish to prove.

␈↓ ↓H␈↓↓To prove ␈↓πF␈↓↓ we proceed by induction on n  There are 2 cases, ␈↓αn|␈↓↓u and ¬qn u.